package proof;

import formula.Formula;
import java.util.ArrayList;

//用于Formula的推导（Derivation for Formula）
//显示结果
public class DerivedProof extends Proof{
    private ArrayList<Proof> conditions;
    private ProofRule rule;

    public DerivedProof(ArrayList<Proof> conditions, ProofRule rule) {
        this.conditions = conditions;
        this.rule = rule;
        this.conclusion = rule.applyRule(conditions);
    }

    public DerivedProof(ArrayList<Proof> conditions, ProofRule rule, Formula conclusion){
        this.conditions = conditions;
        this.rule = rule;
        this.conclusion=conclusion;
    }

    @Override
    public String toString() {
        StringBuilder ret = new StringBuilder("[{");
        for (int i = 0; i < conditions.size(); i++) {
            if (i != 0) {
                ret.append(",");
            }
            ret.append(conditions.get(i).toString());
        }
        ret.append("}").append(rule.getRuleName()).append(" -> ").append(conclusion).append("]");
        return ret.toString();
    }

    @Override
    public String toLatex(){
        StringBuilder ret = new StringBuilder("\\frac{");
        for (int i = 0; i < conditions.size(); i++) {
            if (i != 0) {
                ret.append("\\quad");
            }
            ret.append(conditions.get(i).toLatex());
        }
        ret.append("}{").append(conclusion).append("}{").append(rule.getRuleName()).append("}");
        return ret.toString();
    }
}
